---------------------------------------------

Paper: 5
Title: A Tool-supported Refinement Methodology for Object-oriented Data Models

-------------------- review 1 --------------------

PAPER: 5
TITLE: A Tool-supported Refinement Methodology for Object-oriented Data Models

OVERALL RATING: -1 (weak reject) 
REVIEWER'S CONFIDENCE: 1 (low) 
This paper is in the scope of SLE: 1 (very poor)
Technical Strength: 3 (fair)
Conceptual Novelty: 3 (fair)

----------------------- REVIEW --------------------

This paper discusses the analysis and refinement of object-oriented
specifications using UML/OCL.  The refinement methodology is supported
by a tool.  

Although the paper is globally well written and well structured (I
would only point out the two possible typos in page 3 (last paragraph):
"Person is" -> "Person are" and page 5 (first par) "set type .. set" ->
"set .. set"), I think this it seems not quite relevant to the theme
of SLE conference. A more suitable place for this paper should be the
Models Conference. 

-------------------- review 2 --------------------

PAPER: 5
TITLE: A Tool-supported Refinement Methodology for Object-oriented Data Models

OVERALL RATING: -2 (reject) 
REVIEWER'S CONFIDENCE: 3 (high) 
This paper is in the scope of SLE: 3 (fair)
Technical Strength: 2 (poor)
Conceptual Novelty: 3 (fair)

----------------------- REVIEW --------------------

The paper is potentially interesting, providing a potentially-workable integration of UML-OCL and Isabelle-HOL.  However, the paper is way beyond the anticipated readership of this workshiop.  Furthermore the OCL is inconsistently inaccurate.

To substantiate these comments, the following detailed points arise from the first 4-5 pages:

1.  Bullet 1: the authors assume a formal semantics for UML-OCL (and there are such), but they do not cite the formal semantics that they use.  This makes verification of the validity of the semantic mappings difficult.

[This is plain wrong. We say at several places that we refer to [12] as basis. ]

2.  The authors alledge that UML can describe dynamic system properties: it does not (not least because it has no agreed behavioural semantics): it merely provides the notations for defining static structures of interaction and state machines.

[There are SEVERAL formal semantics for state machines and a bunch of tools
that take UML statemachines and interpret them in a particular way. Anyway,
this is not the TOPIC OF THIS PAPER.]

3. Fig 1: the text explains the diagram in some detail but does not consider the perhaps counterintuitive inheritance association between co-chair and chair.  (There are a number of typos in the description, as well.)

4.  The name invariant on Person is not OCL according to any of the current descriptions.  The errors are in concrete syntax, but also in conception ( name <> '' is not sufficient to define empty name spaces in OCL).

[This is plain wrong. OCL as a standard leaves the possibility to have
alternative syntaxes. 
Independently, it is common practice to use
mathematical notation in papers for programming language notation.
There are actually LaTeX packages supporting this form of paraphasing.]

5.  All the other OCL on pp3-5 contains similar errors of concrete syntax and conceptualisation.  The authors should consult any user of OCL for details.

[The shown syntax was actually parsed by our  tool.]

6.  The authors need to be clearer about the usage of Isabelle-HOL - what communities, for what purposes -  give some examples, so that the SLE community can follow this up if wanted.

7.  At the risk of being called an "ignorant reviewer", I think the use of Hilbert operators is wrong - at least in the mathematical convention.  In any case, I suspect that the majority of the SLE community is unfamiliar with this branch of mathematics/quantum information theory.

[Factual nonsense. The Hilbert operator just picks an arbitrary
element out of a collection and is unspecified in none exists.]

8.  Following from the above, if we are operating in Hilbert space, it might be more expected that a tensor product is appropriate.  This is not an area that I know well, and I am not sure how Cartesian products and Hilbert spaces relate.

9.  Following on from the Hilbertian work, the authors slip unannounced in to category theory (fst etc are not "usual" operators elsewhere, I think?).  I have yet to meet anyone in this community who can speak knowledgeably about category theory, so a little more background is needed.

[Factual Nonsense. Are you in a  "war on tuples" ? fst and snd is used, eg.
in any functional programming language I know of, and, btw., it has 
been introduced in the formal preliminary section. ]

10.  To the target community, the last paragraph of section 2.2 will read like an attempt to use the full character set of the Latex Math mode (and convey little other information).

I am afraid I have to recommend rejection to this entertaining paper, as it would not be comprehendable by the target community. 

-------------------- review 3 --------------------

PAPER: 5
TITLE: A Tool-supported Refinement Methodology for Object-oriented Data Models

OVERALL RATING: -1 (weak reject) 
REVIEWER'S CONFIDENCE: 3 (high) 
This paper is in the scope of SLE: 3 (fair)
Technical Strength: 3 (fair)
Conceptual Novelty: 3 (fair)

----------------------- REVIEW --------------------

This paper is hard to understand (at least for me).
The authors present an approach for refining object-oriented models. They reuse an existing
tool framework based on HOL-OCL to check correctness of the refinement.

As far as I understand, the authors start with an UML class diagram enriched by OCL constraints
to specify invariants as well as the behaviour of operations by pre-/post-conditions.

The authors call this "object-oriented data models" - why is this a data model?

In figure 1, they start with a small class diagram as an example. In my view, this example
is not very convincing, as I do not understand why findRole is an appropriate operation of
a session?

The association roles "person" and "role" are superfluous, as the names of corresponding
classes might be used in  OCL expressions as well.

The role name "participates" is missing. It is used in the definition of the OCL operation
on page 4.

Chapter 3 speaks about "consistency" of class models (the same as the data models in the title?). Hard to understand for a reviewer why s/he should continue to read as the authors
write " ... we concentrate on a specific kind of consistency that is desirable, but strictly
speaking not required by the data refinement methodology we present later".

What is missing in the paper, is a clear and understandable flow of thoughts. I have no
idea how the second paragraph in chapter 3 relates to the first paragraph.

Also, motivations are missing: First sentence of section 3.1: "on the semantic side, we 
need constraints on stats, not state transitions,..."  WHY??

The authors call a class model consistent, if each class can be instantiated. Also here,
no motivating arguments why this definition of consistency makes sense. 

There is a lot of literature in the field on the notion of consistency of UML models.
Nothing is cited here.

Packages don't have instances and are only used on the class level. I understand 
definitions of refinements for classes, but what is meant by refinements of packages??

I have the impression that in Figure 3 the two role names sessions and participants 
have to be exchanged.

I don't understand the specification of findRole for ConcreteSimpleChair.

Section 4.3: The opposite inclusion relations for public classes and public operations
should be explained

I miss a reference to 
- Derrick, John, Boiten, Eerke A.: Refinement in Z and Object-Z